{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances,
  TypeOperators, GADTs, QuasiQuotes, ScopedTypeVariables, TemplateHaskell,
  FlexibleInstances, MultiParamTypeClasses #-}

{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fcontext-stack=250 #-}

module Data.Yoko.Zipper where

import Data.Yoko.ReflectBase

import Data.Yoko.ZipperHelp

pamf x = flip fmap x

-- #1 in some * expression, at a * expression (e.g. in the Int of [(Int, Char)])
--   * check: see Zip below
-- #2 in a constructor, at a particular field (e.g. in the second field of (:))
--   * thinking this would take place "inside" of Zip, e.g. DT (At a path),
--     using the Core types to pause in between fields
--   * could make an interesting cursor navigation, nextField, that moves to
--     the next field
--   * could make an interesting cursor navigation, seekR, that finds the next
--     recursive occurrence

-- TODO can I lift the Zip1/Zip2 constraints out of CxtIn and expose them via
-- some sort of type family like (Zips a path ::: All ZipTurnU)
--
--  type family Zips a path
--  type instance Zips a Top = V
--  type instance Zips (t a)   (In1 :< path) = N (t a, In1)   :+ Zips a path
--  type instance Zips (t a b) (In2 :< path) = N (t a b, In2) :+ Zips a path
--
--  data ZipTurnU tturn where ZipTurnU :: ZipTurn turn t => ZipTurnU (t, turn)
--
--  type family TurnCxt turn t
--  type instance TurnCxt In1 (t a)   = Cxt1 t a
--  type instance TurnCxt In2 (t a b) = Cxt2 t a b
--
--  type family ArgCxt turn t
--  type instance ArgCxt In1 (t a)   = a
--  type instance ArgCxt In2 (t a b) = a
--
--  class ZipTurn turn t where
--    fill :: [qP|turn|] -> TurnCxt turn t -> ArgCxt turn t -> t
--  instance Zip1 t => ZipTurn [qP|In1|] (t a)   where fill _ = fill1
--  instance Zip2 t => ZipTurn [qP|In2|] (t a b) where fill _ = fill2

-- TODO consider
--   http://hackage.haskell.org/packages/archive/zipper/0.3.1/doc/html/src/Generics-MultiRec-Zipper.html

type family Cxt1 (t :: * -> *) a
class Zip1 t where
  fill1 :: Cxt1 t a -> a -> t a
  next1 :: [qP|t :: *->*|] -> Cxt1 t a -> a -> Maybe (Cxt1 t a, a)
  into1 :: t a -> Maybe (a, Cxt1 t a)
  -- TODO abstract over Maybe, use a "sup" to drive natural transformations for
  -- the types of the conglomerate functions

type family Cxt2 (t :: * -> * -> *) a b
class Zip2 t where
  fill2 :: Cxt2 t a b -> a -> t a b
  into2 :: t a b -> Maybe (a, Cxt2 t a b)

data Top; data In1; data In2; data InDC dc; infixr 5 :<; type (:<) = (,)

type family At a path
type instance At a Top = a
type instance At (t a)   (In1 :< path) = At a path
type instance At (t a b) (In2 :< path) = At a path
type instance At t       (InDC fds :< path) = At (Gst (FieldRep (Leftmost fds))) path

type family Init ts
type instance Init (t :< Top) = Top
type instance Init (t :< u :< ts) = t :< Init (u :< ts)

type instance Append Top b = b
type instance Append (c :< d) b = c :< Append d b

type family Snoc path t
type instance Snoc Top t = t :< Top
type instance Snoc (turn :< path) t = turn :< Snoc path t

type family Last path
type instance Last (turn :< Top) = turn
type instance Last (turn :< (turn' :< path)) = Last (turn' :< path)

data Cxt a path where
  Top :: Cxt a Top
  In :: (At a (turn :< path) ~ At (At a (turn :< Top)) path
        ) => CxtIn a turn -> Cxt (At a (turn :< Top)) path -> Cxt a (turn :< path)

-- data Field dc n -- a field is a constructor paired with a natural
-- (left-to-right)

data CxtIn a turn where
  -- TODO can In1 and In2 be replaced by (computed?) subsets of fields?
  --      e.g.: NP (N dc1 :+ N dc2 :+ ...) Fields
  --      type instance Fields dc1 = N Z :+ N (S (S Z))
  --      type instance Fields dc2 = N (S Z)
  --      et cetera
  In1  :: Zip1 t => Cxt1 t a     -> CxtIn (t a)   In1
  In2  :: Zip2 t => Cxt2 t a b   -> CxtIn (t a b) In2
  -- TODO InDC can be generalized to a subset of fields
  InDC :: All (IndexToIn (FieldRep (Leftmost fds)) (Range (Fst (Leftmost fds)))) fds ->
          CxtDC t fds frames -> CxtIn t (InDC fds)

data IndexToIn c t fd where
  IndexToIn :: (DC (Fst fd), c ~ Index (Snd fd) (Rep (Fst fd)), t ~ Range (Fst fd)) => IndexToIn c t fd

-- | @path@ inhabits @NoRs c@ if following the path through @c@ does not turn
-- through an @R@ /until it exits the current family's structure/ -- i.e. the
-- path turns through a D (c.f. NoRs_D) or the f of an F (c.f. NoRs_2F)
data NoRs c path where
  NoRs_R :: NoRs (R t) Top
  NoRs_D :: NoRs (D a) path
  NoRs_2F :: NoRs (F f c) (In2 :< path)
  NoRs_1F :: NoRs c path -> NoRs (F f c) (In1 :< path)
  NoRs_1FF :: NoRs d path -> NoRs (FF ff c d) (In1 :< path)
  NoRs_2FF :: NoRs c path -> NoRs (FF ff c d) (In2 :< path)
  NoRs_M :: NoRs c path -> NoRs (M i c) path

instance Top ::: NoRs (R t) where inhabits = NoRs_R
instance (turn, path) ::: NoRs (D a) where inhabits = NoRs_D
instance ((turn :< path) ::: NoRs c) => (turn, path) ::: NoRs (M i c) where
  inhabits = NoRs_M inhabits
instance (path ::: NoRs c) => (In1, path) ::: NoRs (F f c) where
  inhabits = NoRs_1F inhabits
instance (path ::: NoRs d) => (In1, path) ::: NoRs (FF ff c d) where
  inhabits = NoRs_1FF inhabits
instance Generic a => (In2, path) ::: NoRs (F (f a) c) where
  inhabits = NoRs_2F
instance (path ::: NoRs c) => (In2, path) ::: NoRs (FF ff c d) where
  inhabits = NoRs_2FF inhabits

data CxtDC t fds frames where
  CxtDC_Base :: (n ~ Len (TakeGsts n dc), Gist (Index n (Rep dc)),
                 Take n (Rep dc) ::: Fds, Drop (S n) (Rep dc) ::: Fds) =>
    Uni fds (dc, n) -> DCOf t dc -> LT n (Rep dc) ->
    TakeGsts n dc -> DropGsts (S n) dc -> CxtDC t fds Top
  CxtDC_Step :: (t ~ Range (Fst (Leftmost fds'))) =>
    NoRs (FieldRep (Leftmost fds')) path ->
    Cxt t (InDC fds' :< path) -> CxtDC (At t (InDC fds' :< path)) fds frames ->
    CxtDC t fds (InDC fds' :< frames)
  -- NB the NoRs inhabitation is not essential, but ensures an /intended/
  -- invariant: recursion within this same family of types takes place only in
  -- the @CxtDC@ argument

fillIn :: CxtIn a turn -> At a (turn :< Top) -> a
fillIn (In1 c1) = fill1 c1; fillIn (In2 c2) = fill2 c2
fillIn (InDC all cdc) = fillDC all cdc

fillDC :: forall a fds frames.
          All (IndexToIn (FieldRep (Leftmost fds))
                           (Range (Fst (Leftmost fds)))) fds ->
          CxtDC a fds frames -> Gst (FieldRep (Leftmost fds)) -> a
fillDC idxto (CxtDC_Base fds dcof@DCOf{} lt left right) x =
  case instantiate idxto fds of
    IndexToIn -> fr_DCOf dcof $ obj $ core2RMI $
                 appendAFs lt (frips left) (frip x) (frips right)
fillDC idxto (CxtDC_Step _ c cdc) x = fill c $ fillDC idxto cdc x

fill :: Cxt a path -> At a path -> a
fill Top = id
fill (In cin c) = fillIn cin . fill c

data Zip a path = Zip (At a path) (Cxt a path)
here :: Zip a path -> At a path; here (Zip x _) = x
upd :: (At a path -> At a path) -> Zip a path -> Zip a path
upd f (Zip a c) = Zip (f a) c
top :: Zip a path -> a; top (Zip x c) = fill c x

up :: Zip a (turn :< path) -> Zip a (Init (turn :< path))
up (Zip x c) = w x c where
  w :: At a (t :< p) -> Cxt a (t :< p) -> Zip a (Init (t :< p))
  w x (In cin Top) = Zip (fillIn cin x) Top
  w x (In cin c@(In _ _)) = case w x c of
    Zip x c -> case cin of
      In1{} -> Zip x $ In cin c; In2{} -> Zip x $ In cin c
      InDC{} -> Zip x $ In cin c

type Arg1 a path = At a (Snoc path In1)
down1 :: forall t a path. (Zip1 t, At a path ~ t (Arg1 a path)) =>
         Zip a path -> Maybe (Zip a (Snoc path In1))
down1 (Zip x c) = w x c where
  w :: forall a path. (At a path ~ t (Arg1 a path)) =>
       At a path -> Cxt a path -> Maybe (Zip a (Snoc path In1))
  w x Top = pamf (into1 x) $ \(x, c1) -> Zip x $ In (In1 c1) Top
  w x (In cin c) = case cin of
    In1{} -> pamf (w x c) $ \(Zip x c) -> Zip x $ In cin c
    In2{} -> pamf (w x c) $ \(Zip x c) -> Zip x $ In cin c
    InDC{} -> pamf (w x c) $ \(Zip x c) -> Zip x $ In cin c

type Arg2 a path = At a (Snoc path In2)
down2 :: forall t a path. (At a path ~ t (Arg2 a path) (Arg1 a path), Zip2 t
         ) => Zip a path -> Maybe (Zip a (Snoc path In2))
down2 (Zip x c) = w x c where
  w :: forall a path. (At a path ~ t (Arg2 a path) (Arg1 a path)) =>
       At a path -> Cxt a path -> Maybe (Zip a (Snoc path In2))
  w x Top = pamf (into2 x) $ \(x, c2) -> Zip x $ In (In2 c2) Top
  w x (In cin c) = case cin of
    In1{} -> pamf (w x c) $ \(Zip x c) -> Zip x $ In cin c
    In2{} -> pamf (w x c) $ \(Zip x c) -> Zip x $ In cin c
    InDC{} -> pamf (w x c) $ \(Zip x c) -> Zip x $ In cin c



data Disc t path where
  Disc :: SiblingOf t (Range dc) -> DCOf (Range dc) dc ->
          LT n (Rep (Range dc)) -> Cxt t (Snoc path (InDC (N (dc, n)))) -> Disc t path

discriminateDC :: forall turn path fds t dc n a. (Last (turn :< path) ~ InDC fds) =>
  Cxt t (turn :< path) -> Disc t (Init (turn :< path))
discriminateDC = undefined
{-discriminateDC c k = w id where
  w :: forall t' turn' path'. (Last (turn' :< path') ~ InDC fds) => 
       (Disc t' (Init (turn' :< path')) -> Disc t (Init (turn :< path))) ->
       Cxt t' (turn' :< path') -> Disc t (Init (turn :< path)
  w k (In cin c) = case c of
    Top -> case cin of
      InDC _ cdc -> w2 cdc where
        w2 :: CxtDC t'' fds frames -> Disc t' (Init (turn' :< path'))
        w2 (CxtDC_Base u _ _ _ _) = undefined-}

    


situate :: (At t path ~ s, At s path' ~ At t (Append path path')) =>
           Cxt t path -> Zip s path' -> Zip t (Append path path')
situate c (Zip a c') = Zip a $ appendCxt c c'

appendCxt :: forall t path s path'.
             (At t path ~ s, At t (Append path path') ~ At s path') =>
             Cxt t path -> Cxt s path' -> Cxt t (Append path path')
appendCxt = w id where
  w :: forall t2 path2. (At t2 path2 ~ s) =>
       (Cxt t2 (Append path2 path') -> Cxt t (Append path path')) ->
       Cxt t2 path2 -> Cxt s path' -> Cxt t (Append path path')
  w acc Top = acc
  w acc (In cin c) = flip w c $ acc . case cin of
    In1{} -> In cin; In2{} -> In cin; InDC{} -> In cin



--discriminate :: DT t => t -> (DCOf t dc, Nat n, Zip t (InDC (fds :< Top))
--discriminate = undefined




in1 :: Zip1 t => Cxt1 t a -> Cxt a path -> Cxt (t a) (In1 :< path)
in2 :: Zip2 t => Cxt2 t a b -> Cxt a path -> Cxt (t a b) (In2 :< path)
inDC :: (fds ::: All (IndexToIn (FieldRep (Leftmost fds))
                                  (Range (Fst (Leftmost fds))))) =>
        CxtDC a fds frames -> Cxt (Gst (FieldRep (Leftmost fds))) path ->
        Cxt a (InDC fds :< path)
in1 = In . In1; in2 = In . In2; inDC = In . InDC inhabits

in1_ :: Zip1 t => [qP|t :: * -> *|] ->
        Cxt1 t a -> Cxt a path -> Cxt (t a) (In1 :< path)
in2_ :: Zip2 t => [qP|t :: * -> * -> *|] ->
        Cxt2 t a b -> Cxt a path -> Cxt (t a b) (In2 :< path)
in1_ _ = In . In1; in2_ _ = In . In2

dcStep :: (t ~ Range (Fst (Leftmost fds')),
           path ::: NoRs (FieldRep (Leftmost fds'))
          ) => Cxt t (InDC fds' :< path) ->
               CxtDC (At t (InDC fds' :< path)) fds frames ->
               CxtDC t fds (InDC fds' :< frames)
dcStep = CxtDC_Step inhabits
type Fd dc n = N (dc, n)
dcBase :: (DC dc, LessThan n (Rep dc), n ~ Len (TakeGsts n dc),
           Gist (Index n (Rep dc)),
           Take n (Rep dc) ::: Fds, Drop (S n) (Rep dc) ::: Fds) =>
          DCU (Range dc) dc -> TakeGsts n dc -> DropGsts (S n) dc ->
          CxtDC (Range dc) (Fd dc n) Top
dcBase x = CxtDC_Base (Uni (Here Refl)) (DCOf x) lessThan




type instance Cxt1 [] a = ([a], [a])
instance Zip1 [] where
  fill1 (as, bs) a = reverse as ++ a : bs
  into1 [] = Nothing
  into1 (a : as) = Just $ (a, ([], as))
  next1 _ (as, bs) a = case bs of
    [] -> Nothing
    b : bs -> Just ((a : as, bs), b)

type instance Cxt1 Maybe a = ()
instance Zip1 Maybe where
  fill1 = const Just; next1 _ _ _ = Nothing; into1 = fmap $ flip (,) ()

type instance Cxt1 ((,) a) b = a
instance Zip1 ((,) a) where
  fill1 = (,)
  into1 (a, b) = Just (b, a)
  next1 _ _ _ = Nothing

type instance Cxt1 (Either a) b = ()
instance Zip1 (Either a) where
  fill1 = const Right; next1 _ _ _ = Nothing
  into1 (Right a) = Just (a, ())
  into1 _ = Nothing



type instance Cxt2 (,) a b = b
instance Zip2 (,) where fill2 = flip (,); into2 = Just

type instance Cxt2 Either a b = ()
instance Zip2 Either where
  fill2 = const Left
  into2 (Left a) = Just (a, ())
  into2 _ = Nothing

-- TODO this Cxt2 instance just manages siblings, not ancestors/path
data Whacky a b = NilW | AConsW a (Whacky a b) | BConsW b (Whacky a b)
type instance Cxt2 Whacky a b = Whacky a b
instance Zip2 Whacky where
  fill2 = flip AConsW
  into2 (AConsW a w) = Just (a, w)
  into2 _ = Nothing -- for BConsW, should it skip to the next AConsW?





type instance Cxt1 (F f) a = Cxt1 f a
instance Zip1 f => Zip1 (F f) where
  fill1 = (F .) . fill1; next1 _ = next1 [qP|f :: *->*|]
  into1 (F x) = into1 x

type instance Cxt1 (FF ff a) b = Cxt1 (ff a) b
instance Zip1 (ff a) => Zip1 (FF ff a) where
  fill1 = (FF .) . fill1; next1 _ = next1 [qP|ff a :: *->*|]
  into1 (FF x) = into1 x

type instance Cxt1 (M i) a = ()
instance Zip1 (M i) where
  fill1 = const M; next1 _ _ _ = Nothing
  into1 (M x) = Just (x, ())

type instance Cxt2 (FF ff) a b = Cxt2 ff a b
instance Zip2 ff => Zip2 (FF ff) where
  fill2 = (FF .) . fill2; into2 (FF x) = into2 x

type instance Cxt2 (:*) a b = Cxt2 (,) a b
instance Zip2 (:*) where
  fill2 = (uncurry (:*) .) . fill2; into2 (x :* y) = into2 (x, y)


obvious_inhabitation ''IndexToIn
